Statecharts were proposed as a visual depiction mechanism for capturing requirements of reactive software such as automotive, avionics and health care software. It is critical that such software is error-free as any defects in such software could potentially cause loss of life as well as loss of business. Model checking technology as mentioned in reference number 6 of the prior-art references is a usual choice for checking such software for defects.
Model checking can prove the absence of certain kinds of errors as opposed to testing, which can only show the presence of errors and not the absence. A model checker is a tool that applies model checking technology. A model checker takes 2 inputs: a model that needs to be checked and a property of the model that needs to be checked. It then determines whether the model satisfies the property. If the model does not satisfy the property, then the model checker outputs a test case for which the property is violated.
There are many free and commercial model checkers. Of these, the only known model checker that can check Statemate statecharts is the Statemate model checker as mentioned in reference number 1 of the prior-art references. To check for the reachability of a state a model checker analyses all states along all paths starting from the set of valid initial states. Large complex models have long paths resulting in a very large number of states to be analysed. This model checker takes weeks to analyze large commercial statemate statechart models (consisting of 100s of charts) and runs out of memory. This is the state explosion problem.
Bounded model checkers address this problem by imposing a bound on the length of paths they analyse. Bounded model checkers analyse all states along all paths but each path is analysed only up to a user-defined length. This limit on the path length allows bounded model checkers to scale up but with a caveat: a state reported as unreachable by a bounded model checker maybe reachable via a path longer than the bound.
An invention known to us which deals with analyzing large commercial statemate statechart model is as follows:
As mentioned in reference number #20 of the prior-art references, Pike et al. describes an application of k-induction for the verification of real time systems. Analysis using k-induction for a given model M, property P and bound k consists of two steps:                1. Base step: Check if P holds in all paths of length k starting from every initial state of M        2. Inductive step: For every path of length k+1 starting from any arbitrary state, check if P is true for the first k states then P is also true for the k+1th state.        
If the above two checks return true then the model M satisfies the property P. Since both the checks analyse only paths of length k and k+1 they can be performed using bounded model checking. k-induction, thus, is a technique that can be used to prove properties using bounded model checking. The second step of k-induction checks paths that start with an arbitrary state s where P holds and explore all possible paths of length k+1 starting with s. If P is violated in a path, then one needs to check if the arbitrary start state s of the path is reachable in the actual model. Ifs is not a reachable state, then the counter example is spurious and one needs to augment the inductive specification with constraints on the state space to prune the observed unreachable states until either P is satisfied or a valid counter example is encountered. If k-induction throws up a path that does not start from an initial state then there are two actions that can be taken:                1. Keep tightening P to exclude spurious initial states from the inductive step or        2. Keep increasing k        
However, both of the above steps may not scale up for large systems. Further, in the case of Statemate models k-induction is hardly effective.
Thus, in the light of the above mentioned state of art, it is evident that, there is a need for a system and method which:                analyzes large commercial statemate statechart models in less time and utilizes minimum memory of the computing device;        detects the unreachable states in large commercial statemate statechart model;        proves the unreachability of the unreachable states in the large commercial statemate statechart model;        checks the reachability of the states in the large commercial statemate statechart model; and        successfully verifies all properties such as state reachability of large commercial statemate statecharts models.        